%theoremstyle{plain} \theoremsymbol{\ensuremath{\diamondsuit}}
%\newtheorem{theorem}{Theorem}[section]
%\newtheorem{definition}[theorem]{Definition}

\newcommand{\Fa}{$\Phi_1$}
\newcommand{\Fb}{$\Phi_2$}
\newcommand{\SPLOT}{{\sc Splot}}

\newcommand{\XXX}{\comment{XXX}}

% Rule parts

\newcommand{\mA}{{\bf A}}
\newcommand{\mD}{{\bf D}}
\newcommand{\mC}{{\bf C}}
\newcommand{\mN}{$\overline{\bf N}$}

\newcommand{\rN}{{\bf N}$^r$}
\newcommand{\rA}{\mA$^r$}
\newcommand{\rD}{\mD$^r$}
\newcommand{\rC}{\mC$^r$}


% WRITING AND LISTS
\newcommand{\ignore}[1]{}
\newcommand{\UL}{\noindent}
\newcommand{\LI}{\\ \indent * }
\newcommand{\LLI}{\\ \indent \indent + }
\newcommand{\LLLI}{\\ \indent \indent \indent - }
\newcommand{\comment}[1]{\textcolor{red}{{{#1}}}}
%\newcommand{\comment}[1]{}

% MODELS AND STUFF
\newcommand{\name}[1]{$\mathtt{#1}$} %for names of model elements and variables
\newcommand{\nam}[1]{\mathtt{#1}} 
\newcommand{\feat}[1]{\textbf{#1}} %for features
\newcommand{\rp}[1]{\mbox{#1}} %rule parts


\newcommand{\belnap}[1]{\textsf{#1}\xspace}
\newcommand{\True}{\belnap{True}}
\newcommand{\False}{\belnap{False}}
\newcommand{\Maybe}{\belnap{Maybe}}

% LIFT TABLE
\newcommand{\irrelevant}{any}
\newcommand{\absent}{noMatch}
%\newcommand{\matchNoMay}{Match$\neg\exists$\Maybe}
\newcommand{\matchNoMay}{noMay}
\newcommand{\matchSomeMay}{someMay}
\newcommand{\matchAnyhow}{anyMatch}
\newcommand{\allMaybe}{allMay}
\newcommand{\AddAndAllMaybe}{+allMay}
\newcommand{\sameAsBefore}[1]{={#1}}

% SIMPLE LIFT
\newcommand{\shot}{\mathcal{S}}
\newcommand{\setofsimples}{\shot_\mathcal{R}}
\newcommand{\srule}{\mathcal{R}}

\newcommand{\may}[1]{\underline{{#1}} }
% \newcommand{\may}[1]{\lowercase{{#1}}}
% \newcommand{\may}[1]{{#1}$^M$}
% \newcommand{\may}[1]{$\mu${#1}.}
%\newcommand{\mayE}[1]{\may{$_{\exists}${#1}}}
%\newcommand{\mayA}[1]{\may{$_{\forall}${#1}}}
%\newcommand{\mayE}[1]{$\overline{\mbox{#1}}$}
\newcommand{\mayE}[1]{$\underline{\mbox{#1}}$}
%\newcommand{\mayA}[1]{\underline{{#1}}}
\newcommand{\mayA}[1]{\underline{\underline{#1}}}
\newcommand{\nac}[1]{{#1}$_{\mbox{\tiny{NAC}}}$}


\newcommand{\GTR}[3]{{#1} {#2} $\Rightarrow$ {#3}}
\newcommand{\NAC}[1]{\nac{#1}$\Big|$}
%\newcommand{\ExQ}[1]{|^{_\exists{{\bf {#1}}^m}}}
\newcommand{\ExQ}[1]{|^{_\exists{{\bf {#1}}}}}
%\newcommand{\ExQuant}[2]{\Phi_{{#1}}|^{_\exists{#2}}}
\newcommand{\ExQuant}[2]{\Phi_{{#1}}\ExQ{{#2}}}
\newcommand{\ExQuantMeaning}[2]{\groundPhi{{#1}}{{#2}=F} \vee
\groundPhi{{#1}}{{#2}=T}}

\newcommand{\conj}[1]{\phi_{\bf{#1}}^{and}}
\newcommand{\disj}[1]{\phi_{\bf{#1}}^{or}}
%\newcommand{\disj}[1]{{#1}^{or}}


%EXACT LIFT
\newcommand{\ground}[2]{{#1}$\Big|_{\mbox{{\scriptsize{#2}}}}$}
%\newcommand{\groundPhi}[2]{\Phi_{#1}\Big|_{\mbox{{\scriptsize{#2}}}}}
\newcommand{\groundPhi}[2]{\Phi_{#1}|_{\mbox{{\scriptsize{#2}}}}}

% RULES
\newcommand{\apply}[1]{\stackrel{#1~}{\Longrightarrow}}
%\newcommand{\lifted}[1]{\mathcal{#1}}
\newcommand{\lifted}[1]{#1^\uparrow}

\newcommand{\match}[1]{{\it match}({#1})}
\newcommand{\mdash}{\noindent -- }

\newcommand{\pattern}[1]{\mathbf{#1}}

\newcommand{\context}{C\xspace}


% TUPLES AND SETS
\newcommand{\set}[1]{\{#1\}}
\newcommand{\tuple}[1]{\langle #1 \rangle}


% MAY MODELS
\newcommand{\refines}{\preceq}

%%%%%%%%%%%%%%%%%%%%%

\newcommand{\uset}{\mbox{\sc s}}
\newcommand{\particular}{\mbox{\sc p}}
\newcommand{\variable}{\mbox{\sc v}}
\newcommand{\constant}{\mbox{\sc c}}
\newcommand{\complete}{\mbox{\sc comp }}
\newcommand{\incomplete}{\mbox{\sc inc }}
\newcommand{\present}{\mbox{\sc e}}


\newcommand{\latstyle}[1]{\ensuremath{\mathbf{#1}}}
\newcommand{\below}{\sqsubseteq}
\newcommand{\labove}{\sqsupseteq}
\newcommand{\limp}{\Rightarrow}
\newcommand{\join}{\sqcup}
\newcommand{\meet}{\sqcap}
\newcommand{\bigjoin}{\bigsqcup}
\newcommand{\bigmeet}{\meet}
\newcommand{\Land}{\bigwedge}
\newcommand{\Lor}{\bigvee}
\newcommand{\lsabove}{\sqsupset} % strict above
\newcommand{\lpmi}{\Leftarrow}
\newcommand{\liff}{\Leftrightarrow}

\newcommand{\true}{\mbox{\sc t}}
\newcommand{\false}{\mbox{\sc f}}
\newcommand{\maybe}{\mbox{\sc m}}
\newcommand{\conflict}{\mbox{\sc d}}
\newcommand{\img}{\mbox{\emph{img}}}

% info leq
\newcommand{\ileq}{\preceq}
\newcommand{\igeq}{\succeq}
% truth leq
\newcommand{\tleq}{\below}
\newcommand{\tgeq}{\labove}
\newcommand{\tand}{\land}
\newcommand{\tor}{\lor}
\newcommand{\tneg}{\neg}
\newcommand{\iand}{\meet}
\newcommand{\ior}{\join}
\newcommand{\ineg}{\mathord{-}}
\newcommand{\ttop}{\textsf{{\small t}}\xspace}
\newcommand{\tbot}{\textsf{{\small f}}\xspace}
\newcommand{\itop}{\textsf{{\small d}}\xspace}
\newcommand{\ibot}{\textsf{{\small m}}\xspace}

\newcommand{\cgeq}{\leq}
\newcommand{\cleq}{\geq}

\newcommand{\modify}[2]{\annote[#1]{changed}{#2}}

%The ones below this line are copied from the ME10 paper

% ORIG
% \newtheorem{mydefinition}[theorem]{Definition}
% \newtheorem{myobservation}[theorem]{Observation}
% \newtheorem{myremark}[theorem]{Remark}
% \newtheorem{myproposition}[theorem]{Proposition}
% \newtheorem{myclaim}[theorem]{Claim}
% \newtheorem{mylemma}[theorem]{Lemma}
% \newtheorem{mycorollary}[theorem]{Corollary}
% \newtheorem{myexample}[theorem]{Example}
% \newtheorem{myexamples}[theorem]{Examples}
% \newtheorem{myalgorithm}[theorem]{Algorithm}
% \newtheorem{myconstruction}[theorem]{Construction}
%IEEE
\newtheorem{mytheorem}{Theorem}
\newtheorem{mydefinition}{Definition}
% \newtheorem{myobservation}{Observation}
% \newtheorem{myremark}{Remark}
% \newtheorem{myproposition}{Proposition}
% \newtheorem{myclaim}{Claim}
\newtheorem{mylemma}{Lemma}
% \newtheorem{mycorollary}{Corollary}
% \newtheorem{myexample}{Example}
% \newtheorem{myexamples}{Examples}
% \newtheorem{myalgorithm}{Algorithm}
% \newtheorem{myconstruction}{Construction}


\newcommand{\dashl}{{\stackrel{l}{\dashrightarrow}}}
\newcommand{\dashc}{{\stackrel{c}{\dashrightarrow}}}
\newcommand{\arrl}{{\stackrel{l}{\longrightarrow}}}

\newcommand{\bolddot}{\hspace{-1.5mm}\textbf{.}\ \  }

\newcommand{\BT}{\begin{mytheorem}}
\newcommand{\ET}{\end{mytheorem}}
\newcommand{\BCR}{\begin{mycorollary}\bolddot}
\newcommand{\ECR}{\end{mycorollary}}
\newcommand{\BPR}{\begin{myproposition}\bolddot}
\newcommand{\EPR}{\end{myproposition}}
\newcommand{\BL}{\begin{mylemma}\bolddot}
\newcommand{\EL}{\end{mylemma}}
\newcommand{\BCM}{\begin{myclaim}\bolddot}
\newcommand{\ECM}{\end{myclaim}}

\newcommand{\BD}{\begin{mydefinition}}
\newcommand{\ED}{\end{mydefinition}}
\newcommand{\BPF}{\begin{proof}}
\newcommand{\EPF}{\qed \end{proof}}
\newcommand{\BEX}{\begin{myexample}}
\newcommand{\EEX}{\end{myexample}}
\newcommand{\BEXS}{\begin{myexamples}}
\newcommand{\EEXS}{\end{myexamples}}
\newcommand{\BOB}{\begin{myobservation}}
\newcommand{\EOB}{\end{myobservation}}
\newcommand{\BR}{\begin{myremark}}
\newcommand{\ER}{\end{myremark}}
\newcommand{\BAL}{\begin{myalgorithm}}
\newcommand{\EAL}{\end{myalgorithm}}

\newcommand{\BCO}{\begin{myconstruction}}
\newcommand{\ECO}{\end{myconstruction}}


\newcommand{\BPFSK}{\noindent \textit{Proof Sketch}.\ \ }
\newcommand{\EPFSK}{{\qed}\vspace{2mm}}

%\newcommand{\EPFnoqed}{\end{proof}}

%\newcommand{\BCJR}{\begin{conjecture}}
%\newcommand{\ECJR}{\end{conjecture}}
%\newcommand{\BRM}{\begin{remark}}
%\newcommand{\ERM}{\end{remark}}
%\newcommand{\BEXM}{\begin{example}}
%\newcommand{\EEXM}{\begin{flushright}$\lrcorner$\end{flushright}\end{example}}

\newcommand{\DBPR}{\quad \\ \textbf{Proposition }}
\newcommand{\DEPR}{}
\newcommand{\DBT}{\quad \\ \textbf{Theorem }}
\newcommand{\DET}{}


\newcommand{\BE}{\begin{enumerate}}
\newcommand{\EE}{\end{enumerate}}
\newcommand{\BI}{\begin{itemize}}
\newcommand{\EI}{\end{itemize}}

\newenvironment{Rightitem}{%
 \renewcommand{\labelitemii}{$\Longrightarrow$}%
  \begin{itemize}}{\end{itemize}}
\newenvironment{Leftitem}{%
  \renewcommand{\labelitemi}{$(\Longleftarrow )$}%
    \begin{itemize}}{\end{itemize}}
\newenvironment{Iffitem}{%
  \renewcommand{\labelitemi}{$\Longleftrightarrow$}%
    \begin{itemize}}{\end{itemize}}
\newenvironment{Iffitemi}{%
  \renewcommand{\labelitemii}{$\Longleftrightarrow$}%
    \begin{itemize}}{\end{itemize}}

\newcommand{\BRI}{\begin{Rightitem}\item}  \newcommand{\ERI}{\end{Rightitem}}
\newcommand{\BLI}{\begin{Leftitem}\item}   \newcommand{\ELI}{\end{Leftitem}}
\newcommand{\BIFF}{\begin{Iffitem}\item}   \newcommand{\EIFF}{\end{Iffitem}}
\newcommand{\BIFFI}{\begin{Iffitemi}\item}   \newcommand{\EIFFI}{\end{Iffitemi}}

\newcommand{\myitemi}{\textrm{i}}
\newcommand{\myitemii}{\textrm{ii}}

\newcommand{\bc}{\begin{center}}
\newcommand {\ec}{\end{center}}
\newcommand{\la}{\langle}
\newcommand {\ra}{\rangle}



% \newcommand{\false}{{\textsl{false}}\xspace}
% \newcommand{\true}{{\textsl{true}}\xspace}
\newcommand{\metafalse}{\mathbf{False}}
\newcommand{\metatrue}{\mathbf{True}}
\newcommand{\truestar}{{\bf true}[*]}

\newcommand{\globally}{\textsf{G}}
\newcommand{\eventually}{\textsf{F}}
\newcommand{\weakuntil}{\textsf{W}}
\newcommand{\stronguntil}{\textsf{U}}
\newcommand{\until}{\textsf{U}}

\newcommand{\modelsprop}{\begin{picture}(10,10)\put(1.8,0){\line(0,0){6.5}}
\put(3,0){\line(0,0){6.5}}\put(3,4){\line(4,0){4}}\put(3,2){\line(4,0){4}}\end{
picture}}
%\newcommand{\modelspropimp}{\models}
\newcommand{\nmodelsprop}{\begin{picture}(10,10)\put(0,0){$\modelsprop$}\put(3,
0){$\slash$}\end{picture}}
\newcommand{\modelsbool}{\modelsprop}
\newcommand{\nmodelsbool}{\nmodelsprop}

\newcommand{\mymodels}{\begin{picture}(14,11)\put(3.25,0){$\models$}\end{picture
}}
\newcommand{\nmodels}{\begin{picture}(14,11)\put(3,0){$\models$}\put(6,0){
$\slash$}\end{picture}}
\newcommand{\modelstrue}{\begin{picture}(14,11)\put(3,0){$\models$}\put(6,5){{
\small$\true$}}\end{picture}}
\newcommand{\modelsc}{\begin{picture}(14,11)\put(3,0){$\models$}\put(7,5.5){
\scriptsize$c$}\end{picture}}
\newcommand{\modelsaccept}{\begin{picture}(18,11)\put(3,0){$\models$}\put(12,1){
\scriptsize$\uparrow$}\end{picture}}
\newcommand{\modelsreject}{\begin{picture}(18,11)\put(3,0){$\models$}\put(12,0){
\scriptsize$\downarrow$}\end{picture}}
\newcommand{\nmodelsaccept}{\begin{picture}(18,11)\put(3,0){$\models$}\put(6,0){
$\slash$}\put(12,01){\scriptsize$\uparrow$}\end{picture}}
\newcommand{\nmodelsreject}{\begin{picture}(18,11)\put(3,0){$\models$}\put(6,0){
$\slash$}\put(12,0){\scriptsize$\downarrow$}\end{picture}}

\newcommand{\modelstight}{\begin{picture}(14,11)\put(3.25,0){$|$}\put(3.75,0){
$\equiv$}\end{picture}}
\newcommand{\nmodelstight}{\begin{picture}(14,11)\put(0,0){\modelstight}\put(5,
0){$\slash$}\end{picture}}

\newcommand{\modelsltl}{\begin{picture}(22,11)\put(3,0){$\models$}\put(12,-2){
\scriptsize$\ltl$}\end{picture}}

\newcommand{\modelsw}{\begin{picture}(14,11)\put(3,0){$\models$}\put(7,5.5){
\tiny$-$}\end{picture}}
\newcommand{\modelss}{\begin{picture}(14,11)\put(3,0){$\models$}\put(7,5.5){
\tiny$+$}\end{picture}}
\newcommand{\nmodelsw}{\begin{picture}(14,11)\put(3,0){$\models$}\put(6,-1){
$\slash$}\put(7,5.5){\tiny$-$}\end{picture}}
\newcommand{\nmodelss}{\begin{picture}(14,11)\put(3,0){$\models$}\put(6,-1){
$\slash$}\put(7,5.5){\tiny$+$}\end{picture}}

\newcommand{\modelsb}{\begin{picture}(14,11)\put(3,0){$\models$}\put(7,5.5){
\scriptsize$b$}\end{picture}}
\newcommand{\nmodelsc}{\begin{picture}(14,11)\put(3,0){$\models$}\put(6,0){
$\slash$}\put(6,5.5){\scriptsize$c$}\end{picture}}
\newcommand{\modelscone}{\begin{picture}(14,11)\put(3,0){$\models$}\put(5,5.5){
\scriptsize$c$}\put(8,5.5){\scriptsize$_1$}\end{picture}}
\newcommand{\modelsconetwo}{\begin{picture}(14,12)\put(3,0){$\models$}\put(5,
5.5){\scriptsize$c$}\put(8,5.5){\scriptsize$_1$}\put(5,-2.5){\scriptsize$c$}
\put(8,-2.5){\scriptsize$_2$}\end{picture}}
\newcommand{\nmodelsconetwo}{\begin{picture}(14,12)\put(3,0){$\models$}\put(6,0)
{$\slash$}\put(5,5.5){\scriptsize$c$}\put(8,5.5){\scriptsize$_1$}\put(5,-2.5){
\scriptsize$c$}\put(8,-2.5){\scriptsize$_2$}\end{picture}}
\newcommand{\modelscp}{\begin{picture}(14,12)\put(3,0){$\models$}\put(6,5...5){
\scriptsize$c$}\put(5,-2.5){\scriptsize$p$}\end{picture}}
\newcommand{\nmodelscp}{\begin{picture}(14,12)\put(3,0){$\models$}\put(6,0){
$\slash$}\put(6,5.5){\scriptsize$c$}\put(5,-2.5){\scriptsize$p$}\end{picture}}
\newcommand{\modelstruefalse}{\begin{picture}(14,12)\put(3,0){$\models$}\put(6,
5){\scriptsize$\true$}\put(6,-3.5){\scriptsize$\false$}\end{picture}}
\newcommand{\modelsconec}{\begin{picture}(14,12)\put(3,0){$\models$}\put(6,5.5){
\scriptsize$c$}\put(8,5.5){\scriptsize$_1$}\put(5,-2.5){\scriptsize$c$}\end{
picture}}

\newcommand{\nmodelsf}{\begin{picture}(15,12)\put(3,0){$\models$}\put(6,0){
$\slash$}\put(9,-2){\scriptsize$f$}\end{picture}}
\newcommand{\modelsf}{\begin{picture}(15,12)\put(3,0){$\models$}\put(9,-2){
\scriptsize$f$}\end{picture}}


%\newcommand{\iff}{\Longleftrightarrow}
\newcommand{\projc}{\mbox{$\mid_c$}}
\newcommand{\projcone}{\mbox{$\mid_{c_1}$}}
\newcommand{\comma}{\mbox{$\cdot$}}
\newcommand{\tilda}{\mbox{$\circ$}}
\newcommand{\bbltilda}{\mbox{$\sim$}}
\newcommand{\orr}{\mbox{$\cup$}}
\newcommand{\rand}{\mbox{$\&$}}
\newcommand{\andd}{\mbox{$\cap$}}
\newcommand{\kleene}{\mbox{$^*$}}
\newcommand{\abort}{\mbox{ abort }}
\newcommand{\dualabort}{{\mbox{ dual\_abort }}}
\newcommand{\at}{\mbox{${@}$}}
\newcommand{\ctla}{\textsf{A}}
\newcommand{\ctle}{\textsf{E}}
% \renewcommand{\next}{\textsf{X}}
\newcommand{\strongnext}{\textsf{X!}}
\newcommand{\ex}{\textsf{EX}}
\newcommand{\ax}{\textsf{AX}}
\newcommand{\eg}{\textsf{EG}}
\newcommand{\ag}{\textsf{AG}}
\newcommand{\af}{\textsf{AF}}
\newcommand{\ef}{\textsf{EF}}
\newcommand{\abg}{\textsf{ABG}}
\newcommand{\abf}{\textsf{ABF}}
\newcommand{\nextevent}{\textsf{next\_event}}
\newcommand{\before}{\textsf{before}}
\newcommand{\without}{\textsf{without}}
\newcommand{\including}{\textsf{including}}
\newcommand{\stutter}{\textsf{stutter}}
\newcommand{\infoften}{\textsf{infoften}}
\newcommand{\immbefore}{\textsf{imm\_before}}


\newcommand{\impx}{\begin{picture}(17,10)\put(3.25,0){\line(0,0){5}}\put(3.25,0)
{$\Rightarrow$}\end{picture}}
\newcommand{\imp}{\begin{picture}(17,10)\put(3.25,0){\line(0,0){5}}\put(3...25,
0){$\rightarrow$}\end{picture}}
\newcommand{\sagimp}{\begin{picture}(17,10)\put(3.25,0){$\sim$}\put(7.25,0){
$\tiny{>}$}\end{picture}}
\newcommand{\eqdef}{\stackrel{\tiny{\rm def}}{=}}
\newcommand{\myitem}[1]{\item {#1}}
\newcommand{\nin}{\notindent}

\newcommand{\ctl}{\mbox{\sc ctl}}
\newcommand{\ctlstar}{\mbox{{\sc ctl}$^*$}}
\newcommand{\actl}{\mbox{\sc actl}}
\newcommand{\ltl}{\mbox{\sc ltl}}
\newcommand{\gdl}{\mbox{\sc gdl}}
\newcommand{\logic}{\mbox{\sc sereltl}}
\newcommand{\ltlres}{\mbox{\sc r\_ltl}}

\newcommand{\bdd}{\mbox{\sc bdd}}
\newcommand{\smv}{\mbox{\sc smv}}
\newcommand{\fsm}{\mbox{\sc fsm}}

\newcommand{\fds}{\mbox{\sc fds}}
\newcommand{\ds}{\mbox{\sc dts}}
\newcommand{\dts}{\mbox{\sc dts}}
\newcommand{\dsof}[1]{{{\mathcal{D}}{_{#1}}}}
\newcommand{\buchi}{B$\ddot{\textrm{u}}$chi}
\newcommand{\synpar}{\begin{picture}(10,4)\put(1,0){$|$}\put(3,0){$|$}\put(5,0){
$|$}\end{picture}}
\newcommand{\sat}{\mbox{$\mathcal{S}$}}

%\newcommand{\Implies}{\mbox{$\rightarrow$}}
\newcommand{\Implies}{\models}


\newcommand{\ere}{\mbox{\sc ere}}
\newcommand{\sere}{\mbox{\sc sere}}
\newcommand{\csere}{\mbox{\sc Sere}}
%\newcommand{\serei}{\mbox{\sc sere$^i$}}
%\newcommand{\seresix}{\mbox{\sc sere$^6$}}
\newcommand{\serefive}{\mbox{\sc fre}}
%\newcommand{\serefour}{\mbox{\sc sere$^4$}}
%\newcommand{\serethree}{\mbox{\sc sere$^3$}}
\newcommand{\coresere}{\mbox{\sc re}}
\newcommand{\re}{\mbox{\sc re}}
\newcommand{\pv}{\mbox{\sc pc}}
\newcommand{\mcv}{\mbox{\sc mc}}
\newcommand{\wv}{\mbox{\sc wpc}}
\newcommand{\sv}{\mbox{\sc spc}}

\newcommand{\fail}{\mbox{\sf fail}}



\newcommand{\serestart}{{\cal F}}
\newcommand{\sereend}{{\cal L}}
\newcommand{\serenull}{{\emptyset}}
\newcommand{\serefollow}{{\cal A}}
\newcommand{\serebefore}{{\cal B}}
\newcommand{\serenexts}{{\cal N}}
\newcommand{\sereprev}{{\cal P}}
\newcommand{\pred}{\widetilde{{\cal P}}}
\newcommand{\nexts}{\widetilde{{\cal N}}}
\newcommand{\statepred}{\sc{pred}}

\newcommand{\hatr}{{\hat{r}}}
\newcommand{\tilder}{{\widetilde{r}}}
\newcommand{\stateb}{{s_b}}
\newcommand{\statem}{{s_m}}
\newcommand{\staten}{{state}}
\newcommand{\posinit}{{\lambda_{0}}}
\newcommand{\posacc}{{\lambda_{\infty}}}
%\newcommand{\xsink}{{x_{sink}}}
\newcommand{\stateinit}{{q_{init}}}
\newcommand{\stateacc}{{q_{accept}}}
\newcommand{\statesacc}{{Q_{accept}}}
\newcommand{\statesink}{{q_{sink}}}
\newcommand{\statesinkr}{{q^r_{sink}}}

\newcommand{\pnfa}{\mbox{\sc pnfa}}
\newcommand{\pnfaof}[1]{{\mbox{\sc pnfa}}{\textsc{(}}{#1}{\textsc{)}}}
%\newcommand{\kripke}[1]{{\cal{K}}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\kripke}[1]{{{\mathcal{K}}{_{#1}}}}
\newcommand{\nfaacr}{\mbox{\sc nfa}}
\newcommand{\dfaacr}{\mbox{\sc dfa}}
\newcommand{\gba}{\mbox{\sc gba}}
%\newcommand{\nba}{\mbox{\sc nba}}

\newcommand{\notsr}{\mbox{\small{\sf not}}}
\newcommand{\never}{\mbox{\small{\sf never}}}
\newcommand{\plugstart}{\mbox{\small{\sf start}}}
\newcommand{\plugend}{\mbox{\small{\sf end}}}
\newcommand{\plugmiddle}{\mbox{\small{\sf middle}}}

\newcommand{\lomega}[1]{{{{\cal{L}}^{\omega}}{(}{#1}{)}}}
\newcommand{\lang}[1]{{{{Lng}}{(}{#1}{)}}}
\newcommand{\boolof}[1]{{{{Bool}}{(}{#1}{)}}}
\newcommand{\langrof}[1]{{{{Lang_r}}{(}{#1}{)}}}
\newcommand{\boolrof}[1]{{{B_r}}{(}{#1}{)}}
\newcommand{\stared}[1]{{\cal{S}}{(}{#1}{)}}
\newcommand{\tra}[1]{{\cal{A}}^{c}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\traone}[1]{{\cal{A}}^{c_1}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\trb}[1]{{\cal{B}}^{c}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\trbone}[1]{{\cal{B}}^{c_1}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\trc}[1]{{\cal{T}}^{c}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\trad}[1]{{\cal{T}}^{a,d}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\tradreject}[1]{{\cal{T}}^{a,d\downarrow}{\textsf{(}}{#1}
{\textsf{)}}}
\newcommand{\trda}[1]{{\cal{T}}^{d,a}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\trcad}[1]{{\cal{T}}^{c,a,d}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\trcda}[1]{{\cal{T}}^{c,d,a}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\trconeda}[1]{{\cal{T}}^{c_1,d,a}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\trabnd}[1]{{\cal{T}}^{a\vee(b\wedge\neg d),d}{\textsf{(}}{#1}
{\textsf{)}}}
\newcommand{\trcabnd}[1]{{\cal{T}}^{c,a\vee(b\wedge\neg d),d}{\textsf{(}}{#1}
{\textsf{)}}}
\newcommand{\trcone}[1]{{\cal{T}}^{c_1}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\trans}[1]{{\cal{T}}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\nfaadabortt}[1]{\textsf{abort\_true}^{a,d}{\textsf{(}}{#1}
{\textsf{)}}}
\newcommand{\nfaadabortf}[1]{\textsf{abort\_false}^{a,d}{\textsf{(}}{#1}
{\textsf{)}}}
\newcommand{\nfaaccept}[1]{\textsf{accept}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\nfaadaccept}[1]{\textsf{accept}^{a,d}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\nfareject}[1]{\textsf{reject}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\nfaadreject}[1]{\textsf{reject}^{a,d}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\nfarun}[1]{\textsf{run}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\nfaadrun}[1]{\textsf{run}^{a,d}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\nfa}[1]{{\cal{N}}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\nfaad}[1]{{\cal{N}}^{a,d}{\textsf{(}}{#1}
{\textsf{)}}}
\newcommand{\wit}[1]{{\cal{W}}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\vac}[1]{{\cal{V}}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\vacs}[1]{{\cal{V}s}{\textsf{(}}{#1} {\textsf{)}}}
\newcommand{\qabortf}{q^{\false}}
\newcommand{\qabortt}{q^{\true}}
\newcommand{\qacc}{q^{end}}
\newcommand{\Qacc}{Q^{end}}
\newcommand{\qrej}{q^{rej}}
\newcommand{\Qrej}{Q^{rej}}
\newcommand{\qinit}{q^{0}}
\newcommand{\Qinit}{Q^{0}}
\newcommand{\psik}{\textbf{, }}
\newcommand{\ofail}{\mbox{\textsf{fail}}}
% \newcommand{\st}{\mbox{ such that }}
\newcommand{\w}{\omega}
\newcommand{\pref}{pref}
% \newcommand{\comment}[1]{}
\newcommand{\prefix}[1]{{pref}{(}{#1}{)}}
\newcommand{\pos}[1]{{pos}{(}{#1}{)}}
\newcommand{\letter}[1]{{\ell}{(}{#1}{)}}
%\newcommand{\letters}[1]{{letters}{(}{#1}{)}}
\newcommand{\subof}[1]{{sub}{(}{#1}{)}}
\newcommand{\state}[1]{{state}{(}{#1}{)}}
\newcommand{\stateq}[1]{q_{#1}}

%\newcommand{\atstate}[1]{{at}{(}{#1}{)}}
\newcommand{\atstate}[1]{{at\_}{#1}}
\newcommand{\first}[1]{{\serestart}{(}{#1}{)}}
\newcommand{\last}[1]{{\sereend}{(}{#1}{)}}
\newcommand{\follow}[1]{{\serenexts}{(}{#1}{)}}
\newcommand{\backfollow}[1]{{\sereprev}{(}{#1}{)}}
\newcommand{\pri}{^{\prime}}
\newcommand{\dpri}{^{\prime\prime}}
\newcommand{\tpri}{^{\prime\prime\prime}}
\newcommand{\booleans}{{B}}
\newcommand{\bSigma}{{\Sigma}}
%\newcommand{\atomic}{{P}}
\newcommand{\wordst}{\mbox{s.t.}}
\newcommand{\wordor}{\mbox{or}}
\newcommand{\wordeither}{\mbox{either}}
\newcommand{\wordand}{\mbox{and}}
\newcommand{\wordif}{\mbox{if}}
\newcommand{\wordthen}{\mbox{then}}

\newcommand{\funnyR}{{\cal R}}
\newcommand{\funnyE}{{\cal E}}
\newcommand{\funnyN}{{\cal N}}
\newcommand{\funnyNE}{{\cal NE}}
\newcommand{\funnyF}{{\cal F}}
\newcommand{\funnyS}{{\cal S}}
\newcommand{\funnyD}{{\cal D}}

\renewcommand{\a}{\alpha}
%\renewcommand{\b}{\beta}
\newcommand{\f}{\varphi}
\newcommand{\g}{\psi}
\newcommand{\e}{\epsilon}
\newcommand{\s}{\sigma}
\newcommand{\D}{\mathcal{D}}

\newcommand{\cppcomment}{\quad / \hspace{-3mm} / \hspace{1mm} }
%\newcommand{\w}{\omega}

\newcommand{\stam}[1]{}
\newcommand{\zug}[1]{\langle #1  \rangle}
\newcommand{\N}{\mbox{I$\!$N}}
%\newcommand{\A}{{\mathcal A}}
\newcommand{\calU}{{\mathcal U}}
\newcommand{\V}{\mathcal{V}}
\newcommand{\R}{\mathcal{R}}
\newcommand{\cF}{{\mathcal F}}
\newcommand{\I}{{\mathcal I}}
\newcommand{\cS}{{\mathcal S}}
\newcommand{\C}{{\mathcal C}}
\newcommand{\calG}{{\mathcal G}}
\newcommand{\calF}{{\mathcal F}}
\newcommand{\Lan}{{\mathcal L}}
\newcommand{\A}{{\mathcal A}}
\newcommand{\U}{{\, \mathbf U}\, }
\newcommand{\G}{{\mathbf G}}
\newcommand{\X}{{\mathbf X}}
\newcommand{\W}{{\mathbf W}}
\newcommand{\F}{{\mathbf F}}

\newcommand{\SH}{\mbox{{\it SH}}}
\newcommand{\BH}{\mbox{{\it BH}}}
\newcommand{\BBT}{\mbox{{\it BT}}}
\newcommand{\ST}{\mbox{{\it ST}}}

\newcommand{\ioi}{if and only if }
\newcommand{\es}{\emptyset}
\newcommand{\bd}{\begin{definition}}
\newcommand{\ed}{\end{definition}}
\newcommand{\be}{\begin{enumerate}}
\newcommand{\bi}{\begin{itemize}}
\newcommand{\ee}{\end{enumerate}}
\newcommand{\ei}{\end{itemize}}

\newcommand{\bft}{{\bf true}\xspace}
\newcommand{\bff}{{\bf false}\xspace}

\renewcommand{\vec}{\mathaccent"017E }
